\begin{tabbing}
$\forall$\=$T$:Type, $l$:IdLnk, ${\it ds}_{1}$, ${\it ds}_{2}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$Prop),\+
\\[0ex]$Q$:(State(${\it ds}_{2}$)$\rightarrow\mathbb{N}\rightarrow$Prop), $f$:(State(${\it ds}_{1}$)$\rightarrow\mathbb{N}\rightarrow$$T$).
\-\\[0ex]Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{1}$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}_{2}$)
\\[0ex]$\Rightarrow$ $\neg$destination($l$) $=$ source($l$) $\in$ Id
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{1}$). Dec($\exists$$k$:$\mathbb{N}$. $\neg$$P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{2}$). Dec($\exists$$k$:$\mathbb{N}$. $\neg$$Q$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{1}$), $k$:$\mathbb{N}$. Dec($P$($s$,$k$)))
\\[0ex]$\Rightarrow$ ($\forall$$s$:State(${\it ds}_{2}$), $k$:$\mathbb{N}$. Dec($Q$($s$,$k$)))
\\[0ex]$\Rightarrow$ $\vdash$${\it es}$.\=@source($l$) state ${\it ds}_{1}$ \& ($\forall$$e$:E. kind($e$) $=$ rcv($l$,"tg") $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)\+
\\[0ex]\& @destination($l$) state ${\it ds}_{2}$
\\[0ex]\& ($\forall$$e$:E. kind($e$) $=$ rcv(lnk{-}inv($l$),"tg") $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $\mathbb{Z}$)
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @source($l$) stable $s$.$P$($s$,$k$)  )
\\[0ex]$\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. @destination($l$) stable $s$.$Q$($s$,$k$)  )
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:$\mathbb{N}$.\+
\\[0ex]$\forall$$e$@source($l$).
\\[0ex]$P$(state after $e$,$k$)
\\[0ex]$\Rightarrow$ $\exists$${\it e'}$@destination($l$).$Q$((state when ${\it e'}$),$k$) $\vee$ ($\forall$$n$:$\mathbb{N}$. $Q$(state after ${\it e'}$,$n$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$e$:E.\+
\\[0ex]kind($e$) $=$ rcv(lnk{-}inv($l$),"tg") $\in$ Knd $\Rightarrow$ ($\forall$$k$:$\mathbb{N}$. $k$$<$val($e$) $\Rightarrow$ $P$(state after $e$,$k$)))
\-\\[0ex]$\Rightarrow$ (\=$\forall$$k$:$\mathbb{N}$, $e$:E.\+
\\[0ex]kind($e$) $=$ rcv($l$,"tg") $\in$ Knd
\\[0ex]$\Rightarrow$ val($e$) $=$ $f$((state when sender($e$)),$k$) $\in$ $T$
\\[0ex]$\Rightarrow$ $Q$(state after $e$,$k$))
\-\\[0ex]$\Rightarrow$ $\exists$$e$@destination($l$).True
\\[0ex]$\Rightarrow$ (\=$\forall$$k$:$\mathbb{N}$.\+
\\[0ex]$\exists$$e$@destination($l$).($\forall$$n$:$\mathbb{N}$$_{\mbox{\scriptsize $<$$k$}}$. $Q$((state when $e$),$n$)) $\vee$ ($\forall$$n$:$\mathbb{N}$. $Q$(state after $e$,$n$)))
\-\-
\end{tabbing}